00100	(GIVEAX TRANS
00200	 ((FORALL X)
00300	  ((FORALL Y)
00400	   ((FORALL Z)
00500	    (IMPLIES (AND (EQUAL X Y) (EQUAL Y Z)) (EQUAL X Z))))))
00600	
00700	(GIVEAX SYM
00800	 ((FORALL X) ((FORALL Y) (IMPLIES (EQUAL X Y) (EQUAL Y X)))))
00900	
01000	(GIVEAX REFLEX ((FORALL X) (EQUAL X X)))
01100	
01200	(GIVEAX BIGINTER
01300	 ((FORALL X)
01400	  (IMPLIES
01500	   (AND (ISSET X) ((FORALL Y) (IMPLIES (MEMBER Y X) (ISSET Y))))
01600	   (AND (ISSET (BIGINTER X))
01700		((FORALL Z)
01800		 (EQUIVALENT
01900		  (MEMBER Z (BIGUNION X))
02000		  ((FORALL Y) (IMPLIES (MEMBER Y X)
02100				       (MEMBER Z Y)))))))))
02200	
02300	(GIVEAX BIGUNION
02400	 ((FORALL X)
02500	  (IMPLIES
02600	   (AND (ISSET X) ((FORALL Y) (IMPLIES (MEMBER Y X) (ISSET Y))))
02700	   (AND (ISSET (BIGUNION X))
02800		((FORALL Z)
02900		 (EQUIVALENT
03000		  (MEMBER Z (BIGUNION X))
03100		  ((THEREEXISTS Y)
03200		   (AND (MEMBER Y X) (MEMBER Z Y)))))))))
03300	
03400	(GIVEAX DIFFSET
03500	 ((FORALL X)
03600	  ((FORALL Y)
03700	   (IMPLIES
03800	    (AND (ISSET X) (ISSET Y))
03900	    (AND (ISSET (DIFFERENCE X Y))
04000		 ((FORALL Z)
04100		  (EQUIVALENT
04200		   (MEMBER Z (DIFFERENCE X Y))
04300		   (AND (MEMBER Z X) (NOT (MEMBER Z Y))))))))))
04400	
04500	(GIVEAX FNDEF
04600	 ((FORALL FF)
04700	  ((FORALL U)
04800	   ((FORALL V)
04900	    (IMPLIES
05000	     (AND (ISSET U)
05100		  (ISSET V)
05200		  (ISSET FF)
05300		  (CONTAINED FF (PRODUCT U V))
05400		  ((FORALL X)
05500		   (IMPLIES
05600		    (MEMBER X U)
05700		    ((THEREEXISTS Y)
05800		     (AND (MEMBER Y V) (MEMBER (CONS X Y) FF)))))
05900		  ((FORALL X)
06000		   ((FORALL Y)
06100		    ((FORALL Z)
06200		     (IMPLIES
06300		      (AND (MEMBER X U)
06400			   (MEMBER Y V)
06500			   (MEMBER (CONS X Y) FF)
06600			   (MEMBER (CONS X Z) FF))
06700		      (EQUAL Y Z))))))
06800	     ((THEREEXISTS F)
06900	      (AND (MEMBER F (U (→ V)))
07000		   ((FORALL X)
07100		    (IMPLIES (MEMBER X U)
07200			     (MEMBER (CONS X (α F X)) FF))))))))))
07300	
07400	(GIVEAX EQFN
07500	 ((FORALL U)
07600	  ((FORALL V)
07700	   ((FORALL F)
07800	    ((FORALL G)
07900	     (IMPLIES
08000	      (AND (MEMBER F (U (→ V))) (MEMBER G (U (→ V))))
08100	      (EQUIVALENT
08200	       (EQUAL F G)
08300	       ((FORALL X)
08400		(IMPLIES (MEMBER X U)
08500			 (EQUAL (α F X) (α G X)))))))))))
08600	
08700	(GIVEAX APPLY
08800	 ((FORALL F)
08900	  ((FORALL X)
09000	   ((FORALL U)
09100	    ((FORALL V)
09200	     (IMPLIES (AND (MEMBER F (U (→ V))) (MEMBER X U))
09300		      (MEMBER (α F X) V)))))))
09400	
09500	(GIVEAX POWERSET
09600	 ((FORALL X)
09700	  ((FORALL Y)
09800	   (IMPLIES (AND (ISSET X) (ISSET Y)) (ISSET (X (→ Y)))))))
09900	
10000	(GIVEAX CONTAIN
10100	 ((FORALL U)
10200	  ((FORALL V)
10300	   (EQUIVALENT (CONTAINED U V)
10400		       ((FORALL X)
10500			(IMPLIES (MEMBER X U) (MEMBER X V)))))))
10600	
10700	(GIVEAX PAIR
10800	 ((FORALL X)
10900	  ((FORALL Y)
11000	   ((FORALL U)
11100	    ((FORALL V)
11200	     (EQUIVALENT (EQUAL (CONS X Y) (CONS U V))
11300			 (AND (EQUAL X U) (EQUAL Y V))))))))
11400	
11500	(GIVEAX CARTESIAN
11600	 ((FORALL X)
11700	  ((FORALL Y)
11800	   ((FORALL Z)
11900	    (EQUIVALENT
12000	     (MEMBER Z (PRODUCT X Y))
12100	     ((THEREEXISTS U)
12200	      ((THEREEXISTS V)
12300	       (AND (MEMBER U X)
12400		    (MEMBER V Y)
12500		    (EQUAL Z (CONS U V))))))))))
12600	
12700	(GIVEAX CARTSET
12800	 ((FORALL X)
12900	  ((FORALL Y)
13000	   (IMPLIES (AND (ISSET X) (ISSET Y)) (ISSET (PRODUCT X Y))))))
13100	
13200	(GIVEAX INTER
13300	 ((FORALL X)
13400	  ((FORALL Y)
13500	   ((FORALL Z)
13600	    (EQUIVALENT (MEMBER Z (INTERSECTION X Y))
13700			(OR (MEMBER Z X) (MEMBER Z Y)))))))
13800	
13900	(GIVEAX INTERSET
14000	 ((FORALL X)
14100	  ((FORALL Y)
14200	   (IMPLIES (AND (ISSET X) (ISSET Y))
14300		    (ISSET (INTERSECTION X Y))))))
14400	
14500	(GIVEAX UNIONAX
14600	 ((FORALL X)
14700	  ((FORALL Y)
14800	   ((FORALL Z)
14900	    (EQUIVALENT (MEMBER Z (UNION X Y))
15000			(OR (MEMBER Z X) (MEMBER Z Y)))))))
15100	
15200	(GIVEAX UNIONSET
15300	 ((FORALL X)
15400	  ((FORALL Y)
15500	   (IMPLIES (AND (ISSET X) (ISSET Y)) (ISSET (UNION X Y))))))
15600	
15700	(GIVEAX UNITSET
15800	 ((FORALL X)
15900	  ((FORALL Y) (EQUIVALENT (MEMBER Y (UNITSET X)) (EQUAL Y X)))))
16000	
16100	(GIVEAX NULL1 ((FORALL X) (NOT (MEMBER X NULLSET))))
16200	
16300	(GIVEAX NULLSET (ISSET NULLSET))
16400	
16500	(GIVEAX EXTENSIONALITY
16600	 ((FORALL U)
16700	  ((FORALL V)
16800	   (IMPLIES
16900	    (AND (ISSET U) (ISSET V))
17000	    (IMPLIES ((FORALL X) (EQUIVALENT (MEMBER X U) (MEMBER X V)))
17100		     (EQUAL U V))))))
17200	
17300	(GIVEAX PLUSS
17400	 ((FORALL X)
17500	  ((FORALL Y)
17600	   (IMPLIES
17700	    (AND (MEMBER X I0) (MEMBER Y I0))
17800	    (AND (IMPLIES (EQUAL Y 0) (EQUAL (PLUS X Y) X))
17900		 (IMPLIES
18000		  (NOT (EQUAL Y 0))
18100		  (EQUAL (PLUS X Y) (PLUS (SUCC X) (PRED Y)))))))))
18200	
18300	(GIVEAX INDUCTION
18400	 ((FORALL U)
18500	  (IMPLIES
18600	   (AND (CONTAINED U I0)
18700		(MEMBER 0 U)
18800		((FORALL X) (IMPLIES (MEMBER X U) (MEMBER (SUCC X) U))))
18900	   (EQUAL U I0))))
19000	
19100	(GIVEAX SP
19200	 ((FORALL X)
19300	  (IMPLIES (AND (MEMBER X I0) (NOT (EQUAL X 0)))
19400		   (EQUAL X (SUCC (PRED X))))))
19500	
19600	(GIVEAX PS
19700	 ((FORALL X) (IMPLIES (MEMBER X I0) (EQUAL X (PRED (SUCC X))))))
19800	
19900	(GIVEAX SN0
20000	 ((FORALL X) (IMPLIES (MEMBER X I0) (NOT (EQUAL (SUCC X) 0)))))
20100	
20200	(GIVEAX PRED
20300	 ((FORALL X)
20400	  (IMPLIES (AND (MEMBER X I0) (NOT (EQUAL X 0)))
20500		   (MEMBER (PRED X) I0))))
20600	
20700	(GIVEAX INT0 (MEMBER 0 I0))
20800	
20900	(GIVEAX SUCC
21000	 ((FORALL X) (IMPLIES (MEMBER X I0) (MEMBER (SUCC X) I0))))
21100	
21200	(GIVEAX INTSET (ISSET I0))
21300	
21400	(GIVESCHM COMPREHENSION
21500	 ((PRED PP)
21600	  ((FORALL UU)
21700	   (IMPLIES
21800	    (ISSET UU)
21900	    ((THEREEXISTS WW)
22000	     (AND (ISSET WW)
22100		  ((FORALL XX)
22200		   (EQUIVALENT (MEMBER XX WW)
22300			       (AND (MEMBER XX UU) (PP XX))))))))))
22400	
22500	
22600	(PROOF ONE) 
22700	1 	(USESCHM COMPREHENSION
22800		 ((LAMBDA Y)
22900		  ((FORALL X)
23000		   (IMPLIES (MEMBER X I0)
23100			    (EQUAL (PLUS (SUCC X) Y)
23200				   (SUCC (PLUS X Y)))))))
23300	2 	(US 1 I0)
23400	3 	(USEAX INTSET)
23500	4 	(MP 2 3)
23600	5 	(US 4 A)
23700	6 	(AE 5 1)
23800	7 	(AE 5 2)
23900	8 	(US 7 0)
24000	9 	(USEAX INT0)
24100	10 	(USEAX REFLEX 0)
24200	11 	(USEAX PLUSS X 0)
24300	12 	(TAUT (IMPLIES (MEMBER X I0) (EQUAL (PLUS X 0) X)) 9 10 11)
24400	13 	(UG 12 X)
24450	(MAKETHM P0 13 ONE)
24500	14 	(ASS (MEMBER X I0))
24600	15 	(MP 12 14)
24700	16 	(USEAX REFLEX (SUCC X))
24800	17 	(REPR 16 15 2)
24900	18 	(USETHM P0 (SUCC X))
25000	19 	(USEAX TRANS (PLUS (SUCC X) 0) (SUCC X) (SUCC (PLUS X 0)))
25100	20 	(DED 17 14)
25200	21 	(USEAX SUCC X)
25300	22 	(TAUT (IMPLIES (MEMBER X I0)
25400			       (EQUAL (PLUS (SUCC X) 0) (SUCC (PLUS X 0))))
25500		      21
25600		      20
25700		      19
25800		      18)
25900	23 	(UG 22 X)
26000	24 	(TAUT (MEMBER 0 A) 9 8 23)
26100	25 	(ASS (MEMBER Y A))
26200	26 	(US 7 Y)
26300	27 	(TAUT ((FORALL X)
26400		       (IMPLIES (MEMBER X I0)
26500				(EQUAL (PLUS (SUCC X) Y)
26600				       (SUCC (PLUS X Y)))))
26700		      25
26800		      26)
26900	28 	(US 27 (SUCC X))
27000	29 	(USEAX PLUSS (SUCC X) (SUCC Y))
27100	30 	(USEAX SUCC Y)
27200	31 	(TAUT (MEMBER (SUCC Y) I0) 30 25 26)
27300	32 	(USEAX SN0 Y)
27400	33 	(TAUT (MEMBER Y I0) 25 26)
27500	34 	(TAUT (IMPLIES
27600		       (MEMBER X I0)
27700		       (EQUAL (PLUS (SUCC X) (SUCC Y))
27800			      (PLUS (SUCC (SUCC X)) (PRED (SUCC Y)))))
27900		      29
28000		      33
28100		      30
28200		      32
28300		      21)
28400	35 	(USEAX PS Y)
28500	36 	(MP 35 33)
28600	37 	(REPR 34 36 1)
28700	38 	(USEAX PLUSS X (SUCC Y))
28800	39 	(TAUT (IMPLIES
28900		       (MEMBER X I0)
29000		       (EQUAL (PLUS X (SUCC Y))
29100			      (PLUS (SUCC X) (PRED (SUCC Y)))))
29200		      38
29300		      33
29400		      31
29500		      32)
29600	40 	(REPR 39 36 1)
29700	41 	(MP 14 40)
29800	42 	(USEAX REFLEX (SUCC (PLUS X (SUCC Y))))
29900	43 	(REPL 42 41 2)
30000	44 	(DED 43 14)
30100	45 	(MP 14 21)
30200	46 	(MP 45 28)
30300	47 	(MP 14 37)
30400	48 	(MP 14 44)
30500	49 	(USEAX REFLEX (PLUS (SUCC X) (SUCC Y)))
30600	50 	(REPL 49 47 2)
30700	51 	(REPL 50 46 1)
30800	52 	(REPR 51 48 1)
30900	53 	(DED 52 14)
31000	54 	(UG 53 X)
31100	55 	(AI 31 54)
31200	56 	(US 7 (SUCC Y))
31300	57 	(TAUT (MEMBER (SUCC Y) A) 56 55)
31400	58 	(DED 57 25)
31500	59 	(UG 58 Y)
31600	60 	(US 59 X)
31700	61 	(UG 60 X)
31800	62 	(USEAX CONTAIN A I0)
31900	63 	(TAUT (IMPLIES (MEMBER Y A) (MEMBER Y I0)) 26)
32000	64 	(UG 63 Y)
32100	65 	(US 64 X)
32200	66 	(UG 65 X)
32300	67 	(TAUT (CONTAINED A I0) 62 66)
32400	68 	(USEAX INDUCTION A)
32500	69 	(TAUT (EQUAL A I0) 68 67 24 61)
32600	70 	(REPL 26 69 1)
32700	71 	(TAUT (IMPLIES
32800		       (MEMBER Y I0)
32900		       ((FORALL X)
33000			(IMPLIES
33100			 (MEMBER X I0)
33200			 (EQUAL (PLUS (SUCC X) Y) (SUCC (PLUS X Y))))))
33300		      70)
33400	72 	(ASS (MEMBER Y I0))
33500	73 	(MP 72 71)
33600	74 	(US 73 X)
33700	75 	(DED 74 72)
33800	76 	(TAUT (IMPLIES (AND (MEMBER X I0) (MEMBER Y I0))
33900			       (EQUAL (PLUS (SUCC X) Y) (SUCC (PLUS X Y))))
34000		      75)
34100	77 	(UG 76 Y X)
34200	(MAKETHM TH1 77 ONE)
34300